

Require Import Matrix.Mat.Matrix_Module.
Require Import Reals.
Open Scope R_scope.

Import ListNotations.


(*
  Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A :=
    match n, l with
      | O, x :: l' => x
      | O, other => default
      | S m, [] => default
      | S m, x :: t => nth m t default
    end.

*)
Section Mat_tr.
Variables A:Set.
Variables add :A->A->A.
Variables nil: list A.
(* Fixpoint tr (default:A) (n:nat) ( dlist: list(list A)) :A :=
  match n  with
  | O=>default
  | 1=> nth 0 (nth 0 dlist nil) default 
  | S m=> add (nth m (nth m dlist nil) default) (tr default m dlist )
  end. *)

Fixpoint tr (default:A) (n:nat) ( dlist: list(list A)):=
  match dlist with
  | x::y => add (nth n x default) (tr default (S n) y)
  | nil=> default
  end.

Definition tr_mat (default:A) {n:nat} (Mat:@Mat A n n ):=
  let m := mat A n n  Mat in
  tr default 0 m. 

End Mat_tr.
Section test.
Variable a b c d e f g h i:R.
Definition tm1:= mkMat_3_3 a b c d e f g h i.
Definition tm2:= tr_mat R Rplus 0 tm1.
Lemma tmp: tm2 = a + e + i.
  unfold tm2,tm1,mkMat_3_3,mkMat_3_3',tr_mat.
  simpl. ring.
Qed.

Section Tr_lemma.
Variables A:Set.
Variables Zero:A.
Variables add sub mul:A->A->A.
Variables nil: list A.
Lemma tr_compat : 
  forall {n:nat}  (x x': @Mat A n n), M_eq x x' ->
  tr_mat A add Zero x = tr_mat A add Zero x'.
Proof.
  intros.
  unfold tr_mat.
  rewrite H.
  reflexivity.
Qed.
  


Lemma tr_list_each:forall f1 n i a b,
  length a = n-> length b =n ->
  (forall a, f1 a Zero = a)->
  nth i (list_each A f1 a b) Zero 
  = f1 (nth i a Zero) (nth i b Zero).
Proof.
  induction n.
  - intros. rewrite length_zero_iff_nil in H,H0.
    rewrite H,H0. 
    induction i0. + simpl. rewrite H1. auto.
    + simpl. rewrite H1. auto.
  - induction i0.
    + induction a0. 
      * intros.  inversion H. 
      * induction b0. intros. inversion H0.
        intros. simpl. auto.
    + induction a0. 
      * intros.  inversion H. 
      * induction b0. intros. inversion H0.
        intros. simpl. auto.
Qed.


Lemma tr_mat_each': forall f1 m n i ma mb,
  (forall a,f1 a Zero = a)->
  (height ma = m)->(height mb = m)->
  (width ma n) -> (width mb n) ->
  (forall a b c d, add (f1 a b)(f1 c d) 
    = f1 (add a c) (add b d))->
  tr A add Zero i (mat_each' A f1 ma mb) =
  f1 (tr A add Zero i ma) (tr A add Zero i mb).
Proof.
  induction m. intros.
  - unfold height in H0,H1.
    rewrite length_zero_iff_nil in H0,H1.
    rewrite H0,H1. simpl. rewrite H. auto.
  - induction ma.
    + intros. inversion H0.
    + induction mb.
      * intros. inversion H1.
      * intros. simpl. rewrite <-H4.
        f_equal. apply tr_list_each with(n:=n).
        apply H2. apply H3. assumption.
        apply IHm with(n:=n). assumption.
        inversion H0. auto. inversion H1.
        auto. apply H2. apply H3. assumption.
Qed.
 
(*tr(a+b) = tr(a) + tr(b)*)
Lemma tr_add: forall {n:nat} {ma mb : @Mat A n n},
  (forall a,add a Zero = a)->
  (forall a b c d, add (add a b)(add c d)
    = add (add a c) (add b d))->
  tr_mat A add Zero (matrix_each A add ma mb) =
  add (tr_mat A add Zero ma) (tr_mat A add Zero mb).
Proof.
  intros. unfold tr_mat,matrix_each,mat_each.
  induction ma,mb.
  simpl. apply (tr_mat_each' add n n).
  assumption. apply mat_height. apply mat_height0.
  apply mat_width. apply mat_width0.
  assumption.
Qed.


(*tr(a-b) = tr(a) - tr(b)*)
Lemma  tr_sub: forall {n:nat} {ma mb : @Mat A n n} ,
  (forall a,sub a Zero = a)->
  (forall a b c d, add (sub a b)(sub c d)
    = sub (add a c) (add b d))->
tr_mat A add Zero (matrix_each A sub ma mb) =
sub (tr_mat A add Zero ma) (tr_mat A add Zero mb).
Proof.
  intros. unfold tr_mat,matrix_each,mat_each.
  induction ma,mb.
  simpl. apply (tr_mat_each' sub n n).
  assumption. apply mat_height. apply mat_height0.
  apply mat_width. apply mat_width0. assumption.
Qed.

Lemma nth1:forall (i0:nat) (a0:list A),
  nth (S i0) a0 Zero = nth i0 (tl a0) Zero.
Proof.
  induction i0. induction a0.
  - simpl. auto. - simpl. auto.
  - induction a0. + simpl. auto.
    + simpl. auto.
Qed.

Lemma tr1:forall (m:list (list A))(i0:nat),
  tr A add Zero (S i0) m = tr A add Zero i0 (tailcolumn A m).
Proof.
  induction m. - simpl. auto.
  - intros. simpl. f_equal.
    apply nth1. apply IHm.
Qed.


Lemma tailcolumn_link1:forall n a0 (ma:list (list A)),
  length a0 = n -> 
  length ma = n ->
  tailcolumn A (link1 A a0 ma) = ma.
Proof.
  induction n.
  - intros. rewrite length_zero_iff_nil in H,H0.
    rewrite H,H0. simpl. auto.
  - induction a0. + intros. inversion H.
    + induction ma. * intros. inversion H0.
    * intros. simpl. f_equal. apply IHn. inversion H.
      auto. inversion H0. auto.
Qed. 

Lemma tr_nil_list: forall m i,
  (forall a,add a Zero  = a)->
  tr A add Zero i (nil_list A m) = Zero.
Proof.
  induction m. simpl. auto. induction i0.
  simpl. intros. rewrite <-H.
  f_equal. apply IHm. assumption.
  intros. simpl. rewrite <-H. f_equal. 
  apply IHm. assumption.
Qed.

Lemma tr_gettrans_n:forall (n:nat) (ma:list (list A)),
  (forall a,add a Zero  = a)->
  width ma n->
  tr A add Zero 0 (gettrans A Zero ma n) = 
  tr A add Zero 0 ma.
Proof.
  induction n.
  - intros. simpl. apply width_dlist_0 with(m:=length ma) in H0.
  rewrite H0. rewrite tr_nil_list. auto. assumption. auto.
  - induction ma. + intros. simpl. rewrite gettrans_nil.
    rewrite tr_nil_list. apply H. assumption.
  + intros. simpl. f_equal. induction a0. inversion H0.
    inversion H1. simpl. auto. rewrite gettrans_link1.
    rewrite ?tr1. rewrite tailcolumn_link1 with(n:=n).
    apply IHn. assumption. apply width_tailcolumn.
    apply H0. apply length_tl. apply H0.
    apply height_gettrans. apply length_tl. apply H0.
    apply width_tailcolumn. apply H0.
Qed.
  
Lemma tr_gettrans:forall (n:nat)(m:list (list A)),
  height m = n -> width m n->
  (forall a,add a Zero  = a)->
  tr A add Zero 0 m =
  tr A add Zero 0 (gettrans A Zero m n).
Proof.
  induction n. - intros. unfold height in H.
  rewrite length_zero_iff_nil in H. rewrite H. simpl.
  auto. - induction m. + intros. inversion H.
  + intros. simpl. f_equal.
    { induction a0. simpl. auto.
      simpl. auto. } rewrite ?tr1.
    rewrite gettrans_link1.
    rewrite tailcolumn_link1 with(n:=n).
    rewrite tr_gettrans_n. auto.
    assumption. apply width_tailcolumn. apply H0.
    apply length_tl. apply H0. apply height_gettrans.
    apply length_tl. apply H0. apply width_tailcolumn.
    apply H0.
Qed.  

(*tr(a) = tr(t_a) a的迹等于a的转置的迹*)
Lemma tr_trans: forall {n:nat} (m : @Mat A n n) ,
  (forall a,add a Zero  = a)->
  tr_mat A add Zero m  
  = tr_mat A add Zero (@trans A Zero n n m) .
Proof.
  intros. unfold tr_mat,trans. simpl.
  apply tr_gettrans. apply mat_height. apply mat_width.
  assumption.
Qed.

(* Lemma tr_dl_mul_dl:forall m n ma mb,
  length ma = m -> width ma n ->
  length mb = n-> width mb m ->
  (forall a0 : A, add a0 Zero = a0)->
  tr A add Zero 0
  (dl_mul_dl A Zero add mul ma
     (gettrans A Zero mb n)) =
  tr A add Zero 0
  (dl_mul_dl A Zero add mul mb
     (gettrans A Zero ma m)). 
Proof.
  induction m. + intros. apply length_zero_iff_nil in H.
  rewrite H. simpl. rewrite dl_mul_dl_nil with(m:=n).
  rewrite tr_nil_list. auto. assumption. assumption.
  + induction n. - intros. apply length_zero_iff_nil in H1.
  rewrite H1. simpl. rewrite dl_mul_dl_nil with(m:=S m).
  rewrite tr_nil_list. auto. assumption. apply H.
  - induction ma. * intros. inversion H.
  * induction mb. intros. inversion H1.
    intros. simpl. Admitted.
 *)

(*tr(ab) =  tr(ba)*)
Lemma tr_comm: forall {n m:nat} {ma : @Mat A n m} {mb : @Mat A m n },
  tr_mat A add Zero (matrix_mul A Zero add mul ma mb) =
  tr_mat A add Zero (matrix_mul A Zero add mul mb ma).
Proof.
  intros. unfold tr_mat,matrix_mul,mat_mul_mat. simpl.
  Admitted.
  
  
  

  



(* Section partial_differential. *)
(*矩阵偏导 partial differential*) 

Parameter pd : forall {A:Set}{n m :nat}, A  ->@Mat A n m-> @Mat A n m.

(*pd(tr(a+b))/pd(c)  = pd(tr(a))/pd(c) + pd(tr(b))/pd(c) *)
Axiom pd_add:forall {n m :nat} ( a b:@Mat A n n) (c :@Mat A  n m ) ,
M_eq (pd (tr_mat A add  Zero (matrix_each A add a b)) c) 
(matrix_each A add (pd (tr_mat A add Zero a) c) 
(pd (tr_mat A add Zero b) c)  ).

(*pd(tr(a-b))/pd(c)  = pd(tr(a))/pd(c) - pd(tr(b))/pd(c) *)
Axiom pd_sub:forall {n m :nat} ( a b:@Mat A n n) (c :@Mat A  n m ) ,
M_eq (pd (tr_mat A add Zero (matrix_each A sub a b)) c) 
(matrix_each A sub (pd (tr_mat A add Zero a) c) 
(pd (tr_mat A add Zero b) c)  ).

(* pd( tr(a*c) )/pd(a) =  T_c  *)
Axiom pd_mul:forall (n m :nat) ( a :@Mat A n m) (c :@Mat A  m n ) ,
M_eq (pd (tr_mat A add Zero (matrix_mul A Zero add mul a c) ) a ) 
(@trans A Zero m n c).

(*k个mat相加*)
Definition twoMat {m n:nat} (ma:@Mat A m n): @Mat A m n:=
  matrix_each A add ma ma.

Notation "two* m" := (twoMat m) (at level 60).

Lemma list_each_eq: forall m a b,
  length a = m -> length b = m->
  (forall a0 a2,add a0 a0 = add a2 a2->a0 = a2) ->
  list_each A add a a = list_each A add b b ->
  a = b.
Proof.
  induction m. - intros. rewrite length_zero_iff_nil in H,H0.
  rewrite H,H0. auto. - induction a0. intros. inversion H.
  induction b0. intros. inversion H0. intros. inversion H2.
  apply H1 in H4. f_equal. auto. apply IHm.
  inversion H. auto. inversion H0. auto. assumption.
  auto.
Qed.
  

Lemma mat_each'_eq: forall m n ma mb,
  length ma = m -> length mb = m->
  width ma n -> width mb n->
(forall a0 a2,add a0 a0 = add a2 a2->a0 = a2) ->
  mat_each' A add ma ma =
  mat_each' A add mb mb ->
  ma = mb.
Proof.
  induction m. - intros. rewrite length_zero_iff_nil in H,H0.
  rewrite H,H0. auto. - induction n. + intros. 
  apply width_dlist_0 with(m:=S m) in H1.
  apply width_dlist_0 with(m:=S m) in H2.
  rewrite H1,H2. auto. assumption. assumption.
  + induction ma. * intros. inversion H. *
  induction mb. intros. inversion H0. intros.
  inversion H4. f_equal. apply list_each_eq with(m:=S n).
  apply H1. apply H2. assumption. assumption.
  apply IHm with(n:=S n). inversion H. auto.
  inversion H0. auto. apply H1. apply H2. assumption.
  auto.
Qed.
  

Lemma kMateq: forall {n m:nat} (a b: @Mat A m n) ,
  (forall a0 a2,add a0 a0 = add a2 a2->a0 = a2) ->
M_eq (two* a)  (two* b) -> M_eq a b.
Proof.
  unfold M_eq,twoMat,matrix_each,mat_each.
  simpl. intros. apply mat_each'_eq with(m:=m)(n:=n).
  apply mat_height. apply mat_height. apply mat_width.
  apply mat_width. assumption. apply H0.
Qed.
 


(* b = T_b  ->  pd( tr(a*b*T_a) )/pd(a) =  2ab   *)
Axiom pd_trans_eq:forall (n m :nat) ( a :@Mat A n m) (b :@Mat A  m m) ,
M_eq b  (@trans A Zero m m b) -> 
M_eq (pd (tr_mat A add nil Zero (matrix_mul A Zero add mul (matrix_mul A Zero add mul a b) (@trans A Zero n m a) ) ) a )
( 2 k* (matrix_mul A Zero add mul a b))

(*a与b不相关时，a对b求偏导 = 0*)
Axiom pd_not_correlation:forall (n  m:nat) ( a :@Mat A n n) (b :@Mat A  n m) ,
M_eq (pd (tr_mat A add nil Zero a) b) (MO A Zero n m).

Axiom pd_compat : 
  forall n m, 
     forall x x' : (@Mat A n n) , M_eq x x' ->
        forall y:(@Mat A n m),
         
M_eq (pd (tr_mat A add nil Zero x) y) (pd (tr_mat A add nil Zero x') y) .

Lemma pd_compat' : 
  forall n m, 
     forall x x' : A ,  x = x' ->
        forall y:(@Mat A n m),
         
M_eq (pd x y)  (pd x' y) .
Proof.
intros.
rewrite H.
reflexivity.
Qed.

End Tr_lemma.



(*

Variable A:Set.
Variable Zero:A.
Variable Default:A.
Variable add:A->A->A.
Variable mul:A->A->A.

(*eq_nth*)
(* if la = lb then nth(a) = nth(b)*)
Lemma eq_nth:forall (la lb:list A) (n:nat),
(la = lb) -> nth n la Default = nth n lb Default.
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

(* dlist_tr_eq *)
(* if dla = dlb then tr(dla) = tr(dlb) *)
Lemma dlist_tr_eq: forall (dla dlb:list(list A)) (n:nat),
dla = dlb -> tr A add [] Default n dla = tr A add [] Default n dlb.
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

(* meq_tr_eq *)
(** if A = B then Tr(A) = Tr(B). **)
Lemma meq_tr_eq : forall { n:nat} (ma mb:@Mat A n n),
  (ma === mb) -> tr_mat A add [] Default  ma = tr_mat A add [] Default  mb.
Proof.
  intros.
  unfold tr_mat. rewrite H.
  reflexivity.
Qed.

Lemma nth_add:forall (m : nat) (l1 l2 : list A),
       length l1 = m ->
       length l2 = m ->
       Default = add Default Default ->
       forall n,
       nth n (list_each A add l1 l2) Default = add (nth n l1 Default) (nth n l2 Default).
Proof.
  induction m.
  - induction l1.
    + induction l2.
        induction n.
          simpl. apply H1.
          simpl. apply H1.
        intros. inversion H0.
    + intros. inversion H.
  - induction l1.
    + intros. inversion H.
    + induction l2.
      simpl. intros. inversion H0.
      intros. induction n.
        * simpl. reflexivity.
        * simpl. apply IHl1.
      simpl.
Qed.


Lemma tr_mat_each':forall(n:nat) (ma mb:list (list A)),
height ma = n -> height mb = n ->
width ma  n -> width mb n ->
Default = add Default Default ->
tr A add [] Default n (mat_each' A add ma mb) =
add (tr A add [] Default n ma) (tr A add [] Default n mb).
Proof.
  induction n.
  - intros. simpl. apply H3.
  - induction ma.
    + intros. inversion H.
    + induction mb. 
      * intros. inversion H0.
      * intros. simpl. rewrite nth_add with (n:= S _). 


(*tr(a+b) = tr(a) + tr(b)*)
Lemma tr_add: forall {n:nat} {ma mb : @Mat A n n} ,
tr_mat A add [] Default (matrix_each A add ma mb) = add (tr_mat A add [] Default ma)  (tr_mat A add [] Default mb) .
Proof.
intros.
unfold tr_mat. unfold matrix_each. unfold mat_each. simpl.
rewrite tr_mat_each'. reflexivity.

  
(*tr(a) = tr(t_a) a的迹等于a的转置的迹*)
Lemma tr_trans: forall {n:nat}   {m : @Mat A n n} ,
tr_mat A add [] Default m = tr_mat A add [] Default (trans A Zero m ).
Proof.
  intros.
  unfold tr_mat. unfold mat.
  unfold trans.
 
(*tr(ab) =  tr(ba)*)
Lemma tr_comm: forall {n m:nat} {ma : @Mat A n m} {mb : @Mat A m n },
tr_mat A add [] Default (matrix_mul A Zero add mul ma mb)  
= tr_mat A  add [] Default (matrix_mul A Zero add mul mb ma).
Proof.
  unfold tr_mat,matrix_mul,mat_mul_mat.
  simpl. intros.

(*tr(abc) =  tr(cba)*)
Axiom tr_comm1: forall {n m p:nat}  {ma : @Mat (R->R) n m} {mb : @Mat (R->R) m p } {mc : @Mat (R->R) p n },
tr_mat (R->R)  fadd [] f0 (ma FM* mb FM* mc) = tr_mat (R->R) fadd [] f0 (mc FM* ma FM* mb).
(*tr(abc) =  tr(bca)*)
Axiom tr_comm2: forall {n m p:nat} {ma : @Mat (R->R) n m} {mb : @Mat (R->R) m p } {mc : @Mat (R->R) p n },
tr_mat (R->R)  fadd [] f0 (ma FM* mb FM* mc) = tr_mat (R->R) fadd [] f0 (mb FM* mc FM* ma).

(*tr(cba) =  tr(bca)*)
Axiom tr_comm3: forall {n m p:nat} {ma : @Mat (R->R) n m} {mb : @Mat (R->R) m p } {mc : @Mat (R->R) p n },
tr_mat (R->R) fadd [] f0 (mc FM* ma FM* mb) = tr_mat (R->R) fadd [] f0 (mb FM* mc FM* ma).


Variables Zero:(R->R).
(*tr(a) = tr(t_a) a的迹等于a的转置的迹*)
Axiom tr_trans: forall {n:nat}   {m : @Mat (R->R) n n} ,
tr_mat (R->R) fadd []  f0 m  = tr_mat (R->R) fadd [] f0 (@trans (R->R) Zero n n m) .


(*tr(a+b) = tr(a) + tr(b)*)
Axiom tr_add: forall {n:nat} {ma mb : @Mat (R->R) n n} ,
tr_mat (R->R) fadd [] f0 (ma FM+ mb) = fadd (tr_mat (R->R) fadd [] f0 ma )  (tr_mat (R->R) fadd [] f0 mb ).

(*tr(a-b) = tr(a) - tr(b)*)
Axiom tr_sub: forall {n:nat} {ma mb : @Mat (R->R) n n} ,
tr_mat (R->R) fadd [] f0 (ma FM- mb) = fsub (tr_mat (R->R) fadd [] f0 ma )  (tr_mat (R->R) fadd [] f0 mb ).


(* Section partial_differential. *)
(*矩阵偏导 partial differential*) 

Parameter pd : forall {n m :nat}, (R->R)  ->@Mat (R->R) n m-> @Mat (R->R) n m.

(*pd(tr(a+b))/pd(c)  = pd(tr(a))/pd(c) + pd(tr(b))/pd(c) *)
Axiom pd_add:forall (n m :nat) ( a b:@Mat (R->R) n n) (c :@Mat (R->R)  n m ) ,
pd (tr_mat (R->R) fadd [] f0 (a FM+ b) ) c FM= 
pd (tr_mat (R->R) fadd [] f0 a) c FM+ pd (tr_mat (R->R) fadd [] f0 b ) c  .


(*pd(tr(a-b))/pd(c)  = pd(tr(a))/pd(c) - pd(tr(b))/pd(c) *)
Axiom pd_sub:forall (n m :nat) ( a b:@Mat (R->R) n n) (c :@Mat (R->R)  n m ) ,
pd (tr_mat (R->R) fadd [] f0 (a FM- b) ) c FM= 
pd (tr_mat (R->R) fadd [] f0 a) c FM- pd (tr_mat (R->R) fadd [] f0 b ) c  .

 (* pd( tr(a*c) )/pd(a) =  T_c  *)
Axiom pd1:forall (n m :nat) ( a :@Mat (R->R) n m) (c :@Mat (R->R)  m n ) ,
pd (tr_mat (R->R) fadd [] f0 (a FM* c) ) a FM= (@trans (R->R) Zero m n c).

(* b = T_b  ->  pd( tr(a*b*T_a) )/pd(a) =  2ab   *)
Axiom pd2:forall (n m :nat) ( a :@Mat (R->R) n m) (b :@Mat (R->R)  m m) ,
b FM= @trans (R->R) Zero m m b -> 
pd (tr_mat (R->R) fadd [] f0 (a FM* b FM* @trans (R->R) Zero n m a) ) a FM=  kFM 2 n m (a FM* b).
 

(*a与b不相关时，a对b求偏导 = 0*)
Axiom pd3:forall (n  m:nat) ( a :@Mat (R->R) n n) (b :@Mat (R->R)  n m) ,
pd (tr_mat (R->R) fadd [] f0 a) b FM=  FMO n m.



Axiom Fmat_pd_compat : 
  forall n m, 
     forall x x' : (@FMat n n) , @FMeq n n x x' ->
        forall y:(@FMat n m),
         
pd (tr_mat (R->R) fadd [] f0 x) y FM= pd (tr_mat (R->R) fadd [] f0 x') y .

Lemma Fmat_pd_compat' : 
  forall n m, 
     forall x x' : (R->R) ,  x = x' ->
        forall y:(@FMat n m),
         
pd x y FM= pd x' y .
Proof.
intros.
rewrite H.
reflexivity.
Qed.

Definition feq(f g:R->R):= f = g.
Add Parametric Morphism {m n :nat}: (tr_mat (R->R) fadd []  f0 ) 
  with signature (@FMeq n n) ==> feq  
  as Fmat_tr_mor.
Proof.
exact (@Fmat_tr_compat n ).
Qed.

End tr_lemma.



*)







